(assert (<= 0 (str.len "\u16a7\u01cd\u0125\u2c7b\u0155\u014f\u020b\u16c1\u2c6d\u0211\xf6\u0245\u0224}w\xfc\u16d9\u0248\u16b3") 76))
(check-sat)
